A:Type, eq:EqDecider(A), B:(AType), f, g:a:A fp B(a).
l_disjoint(A;1of(f);1of(g))  f || g 

latex

Definitions	b, t  T, x:A. B(x), EqDecider(T), x(s), (x  l), x. t(x), 1of(t), l_disjoint(T;l1;l2), deq-member(eq;x;L), Prop, P & Q, 2of(t), P  Q, f(x), x  dom(f), f || g, a:A fp B(a), False, A, P  Q
Lemmas	assert-deq-member, assert wf, deq-member wf, l disjoint wf, pi1 wf, l member wf, deq wf